\begin{tabbing}
ecl{-}mng{-}update\=\{i:l\}\+
\\[0ex](${\it es}$; $i$; ${\it ds}$; ${\it da}$; $x$; $z$; ${\it upd}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)\+
\\[0ex]$\Rightarrow$ alle{-}at(\=${\it es}$;\+
\\[0ex]$i$;
\\[0ex]$e$.(\=es{-}after(${\it es}$; $z$; $e$)\+
\\[0ex]=
\\[0ex]list\_accum(\=${\it z'}$,${\it nf}$.let $n$,$f$ = ${\it nf}$\+
\\[0ex]in
\\[0ex]if es{-}bact\=\{i:l\}\+
\\[0ex](${\it ds}$; ${\it da}$; $x$; ${\it es}$; $n$; es{-}init(${\it es}$;$e$); $e$)
\-\\[0ex]then $f$(es{-}state{-}when(${\it es}$; $e$),es{-}val(${\it es}$; $e$))
\\[0ex]else ${\it z'}$
\\[0ex]fi ;
\\[0ex]es{-}when(${\it es}$; $z$; $e$);
\\[0ex]fpf{-}cap(\=${\it upd}$;\+
\\[0ex]product{-}deq(Knd; Id; Kind{-}deq; id{-}deq);
\\[0ex]$<$es{-}kind(${\it es}$; $e$), $z$$>$;
\\[0ex][]))))
\-\-\-\-\-
\end{tabbing}